r, s:RngSig, f:(|r||s|). rng_hom_p(r;s;f)   

latex

Up	rings 1
Definitions of Statement	rng_hom_p(r;s;f)
Definitions	P & Q, rng_hom_p(r;s;f), , t  T, x:A. B(x)
Lemmas	rng sig wf, rng one wf, rng times wf, rng plus wf, rng car wf, fun thru 2op wf